$\forall$$T$:Type, $l$:($T$ List), $i$:\{0..$\parallel$$l$$\parallel^{-}$\}, $j$:\{0..$i$$^{-}$\}. hd(l\_interval($l$;$j$;$i$)) = $l$[$j$] $\in$ $T$